Nuprl Lemma : q-linear_wf
11,40
postcript
pdf
k
:
,
X
:(
),
y
:(
List). (
k
||
y
||)
(q-linear(
k
;
j
.
X
(
j
);
y
)
)
latex
Definitions
x
.
t
(
x
)
,
False
,
A
,
x
(
s
)
,
q-linear(
k
;
i
.
X
(
i
);
y
)
,
t
T
,
A
B
,
P
Q
,
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
i
j
<
k
,
{
i
..
j
}
,
Lemmas
nat
wf
,
int
seg
wf
,
length
wf1
,
rationals
wf
,
select
wf
,
qmul
wf
,
qsum
wf
,
le
wf
,
qadd
wf
origin
k:
, X:(
), y:( List). (k 
||y||) 
(q-linear(k;j.X(j);y) 
) k:, X:(), y:( List). (k ||y||) (q-linear(k;j.X(j);y) ) 
x. t(x)
A T B Qx:A. B(x) j < k
}